T:Type, ll:(T List List), n:{0..||concat(ll)||}.
m:{0..||ll||}
((||concat(firstn(m;ll))||  n)
c ((n - ||concat(firstn(m;ll))||) < ||ll[m]||)
c (concat(ll)[n] = ll[m][(n - ||concat(firstn(m;ll))||)]  T)) 

latex

Definitions	x:A. B(x), ||as||, concat(ll), A  B, firstn(n;as), reduce(f;k;as), Y, A, P  Q, False, t  T, A c B, , x:A. B(x), if b then t else f fi , tt, P  Q, P & Q, P  Q, ff, T, True, SQType(T), {T}, {i..j}, i  j < k, , Unit,
Lemmas	int seg wf, le wf, length wf1, concat wf, firstn wf, select wf, non neg length, length cons, length append, lt int wf, bool wf, iff transitivity, assert wf, eqtt to assert, assert of lt int, le int wf, bnot wf, eqff to assert, squash wf, true wf, bnot of lt int, assert of le int, append wf, select cons tl sq, select append back